\begin{tabbing}
@$i$: with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if eqof(IdDeq)($j$,$i$)$\rightarrow$ with declarations ds:${\it ds}$da:${\it da}$effect of $k$(v) is $x$ := $f$ s v\+
\\[0ex]else  fi
\-
\end{tabbing}